$\forall$${\it es}$:ES, $i$:Id, $P$:(\{$e$:E$\mid$ loc($e$) = $i$\} $\rightarrow\mathbb{P}$).
\\[0ex]$\forall$$e$@$i$. $P$($e$) $\Leftarrow\!\Rightarrow$ ($\forall$$e$@$i$. ($\uparrow$first($e$)) $\Rightarrow$ $P$($e$) \& $\forall$$e$@$i$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ $P$(pred($e$)) $\Rightarrow$ $P$($e$))